Search for: All records

Observations of rapid ongoing grounding line retreat, ice shelf thinning and accelerated ice flow from the West Antarctic Ice Sheet (WAIS) may forebode a possible collapse if global temperatures continue to increase. Understanding and reconstructing West Antarctic Ice Sheet dynamics in past warmer-than-present times will inform about its behavior as an analogue for future climate scenarios. International Ocean Discovery Program (IODP) Expedition 379 visited the Amundsen Sea sector of Antarctica to obtain geological records suitable for this purpose. During the expedition, cores from two drill sites at the Resolution Drift on the continental rise returned sediments whose deposition was possibly influenced by West Antarctic Ice Sheet dynamics from late Miocene to Holocene times. To examine the West Antarctic Ice Sheet dynamics, shipboard physical properties and sedimentological data are correlated with seismic data and extrapolated across the Resolution Drift via core-log-seismic integration. An interval with strongly variable physical properties, high diatom abundance and ice-rafted debris occurrence, correlating with partially high amplitude seismic reflection characteristics was identified between 4.2 and 3.2 Ma. Sedimentation during this interval is interpreted as having occurred during an extended warm period with a dynamic West Antarctic Ice Sheet in the Amundsen Sea sector. These records compare to those of other drill sites in the Ross Sea and the Bellingshausen Sea, and thus suggest an almost simultaneous occurrence of extended warm periods in all three locations. 

This paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the term level, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging: to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We prove that our model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types. 

GADTs can be represented either as their Church encodings a la Atkey, or as fixpoints a la Johann and Polonsky. While a GADT represented as its Church encoding need not support a map function satisfying the functor laws, the fixpoint representation of a GADT must support such a map function even to be well-defined. The two representations of a GADT thus need not be the same in general. This observation forces a choice of representation of data types in languages supporting GADTs. In this paper we show that choosing whether to represent data types as their Church encodings or as fixpoints determines whether or not a language supporting GADTs can have parametric models. This choice thus has important consequences for how we can program with, and reason about, these advanced data types. 

Abstract. The West Antarctic Ice Sheet (WAIS) presently holds enough ice to raise global sea level by 4.3 m if completely melted. The unknownresponse of the WAIS to future warming remains a significant challenge fornumerical models in quantifying predictions of future sea level rise. Sealevel rise is one of the clearest planet-wide signals of human-inducedclimate change. The Sensitivity of the West Antarctic Ice Sheet to a Warmingof 2 ∘C (SWAIS 2C) Project aims to understand past and currentdrivers and thresholds of WAIS dynamics to improve projections of the rateand size of ice sheet changes under a range of elevated greenhouse gaslevels in the atmosphere as well as the associated average globaltemperature scenarios to and beyond the +2 ∘C target of theParis Climate Agreement. Despite efforts through previous land and ship-based drilling on and alongthe Antarctic margin, unequivocal evidence of major WAIS retreat or collapse and its causes has remained elusive. To evaluate and plan for theinterdisciplinary scientific opportunities and engineering challenges thatan International Continental Drilling Program (ICDP) project along the Siple coast near the grounding zone of the WAIS could offer (Fig. 1), researchers, engineers, and logistics providers representing 10 countries held a virtualworkshop in October 2020. This international partnership comprised ofgeologists, glaciologists, oceanographers, geophysicists, microbiologists,climate and ice sheet modelers, and engineers outlined specific researchobjectives and logistical challenges associated with the recovery of Neogene and Quaternary geological records from the West Antarctic interior adjacent to the Kamb Ice Stream and at Crary Ice Rise. New geophysical surveys at these locations have identified drilling targets in which new drilling technologies will allow for the recovery of up to 200 m of sediments beneaththe ice sheet. Sub-ice-shelf records have so far proven difficult to obtainbut are critical to better constrain marine ice sheet sensitivity to pastand future increases in global mean surface temperature up to 2 ∘Cabove pre-industrial levels. Thus, the scientific and technological advances developed through this program will enable us to test whether WAIS collapsed during past intervals of warmth and determine its sensitivity to a +2 ∘C global warming threshold (UNFCCC, 2015).